A:Type, B:(AType), eq:EqDecider(A), f, g:a:A fp B(a), x:A.
x  dom(f  g)  f  g(x) = if x  dom(f) f(x) else g(x) fi  B(x) 

latex

Definitions	P  Q, False, 2of(t), f(x), if b t else f fi, Top, a:A fp B(a), EqDecider(T), f  g, f(x)?z, Unit, P  Q, P & Q, x  dom(f), , Prop, b, A, x(s), x. t(x), x:A. B(x), P  Q, t  T, b
Lemmas	fpf-ap wf, assert wf, not wf, bnot wf, bool wf, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, deq wf, fpf wf, fpf-trivial-subtype-top, top wf, fpf-join wf, fpf-join-dom